\begin{tabbing}
es{-}secret{-}server\=\{\$table:ut2, \$encrypt:ut2, \$decrypt:ut2\}\+
\\[0ex](${\it es}$; $T$; $L$; $i$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it ds}$ = "\$table" : secret{-}table($T$) in \+
\\[0ex](\=$\forall$$l$$\in$$L$.\+
\\[0ex]destination($l$) $=$ $i$
\\[0ex]\& \=state ${\it ds}$\+
\\[0ex]rcv($l$,"\$encrypt"):\=($\mathbb{N}$+Atom1)\+
\\[0ex]$\times$data($T$) sends ["\$encrypt", $e$.next("\$table" when $e$):\=$\mathbb{N}$\+
\\[0ex]$\times$Atom1] on lnk{-}inv($l$)
\-\-\-\\[0ex]\& \=state ${\it ds}$\+
\\[0ex]rcv($l$,"\$decrypt"):\=($\mathbb{N}$+Atom1)\+
\\[0ex]$\times$Atom1 sends ["\$decrypt", $e$.decrypt("\$table" when $e$;val($e$)):data($T$)] on lnk{-}inv($l$))
\-\-\-\\[0ex]\& \=@$i$ only events in map($\lambda$$l$.rcv($l$,"\$encrypt");$L$) change   "\$table" : secret{-}table($T$)\+
\\[0ex]\& \=(\=$\forall$$l$$\in$$L$.\+\+
\\[0ex]@$i$ \=\+
\\[0ex]e\=vents of kind rcv($l$,"\$encrypt") change "\$table" to\+
\\[0ex]$\lambda$$s$,$v$. encrypt($s$."\$table";$v$) State(${\it ds}$) (val:($\mathbb{N}$+Atom1)$\times$data($T$)))
\-\-\-\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]$\exists$${\it e'}$:E.
\\[0ex]$e$ leaks "\$table" to ${\it e'}$
\\[0ex]$\Rightarrow$ \=($\exists$$l$$\in$$L$.kind($e$) $=$ rcv($l$,"\$encrypt") \& kind(${\it e'}$) $=$ rcv(lnk{-}inv($l$),"\$encrypt")\+
\\[0ex]$\vee$ kind($e$) $=$ rcv($l$,"\$decrypt") \& kind(${\it e'}$) $=$ rcv(lnk{-}inv($l$),"\$decrypt"))
\-\-\\[0ex]\& $\forall$$e$@$i$. $\neg$$e$ copies "\$table"
\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]first($e$)
\\[0ex]$\Rightarrow$ \=atoms{-}distinct("\$table" when $e$)\+
\\[0ex]\& ptr("\$table" when $e$) $=$ 0
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$, $j$:Id.\+
\\[0ex]$n$$<\parallel$"\$table" when $e$$\parallel$  $\Rightarrow$ $j$ $>>$ st{-}atom("\$table" when $e$;$n$) $\Rightarrow$ $j$ $=$ $i$)
\-\-\-\-\-\-
\end{tabbing}